1. $T$ : Type \\[0ex]2. $R$ : $T$$\rightarrow$$T$$\rightarrow\mathbb{P}$ \\[0ex]3. $\forall$$a$:$T$. $R$($a$,$a$) \\[0ex]4. $\forall$$a$, $b$:$T$. $R$($a$,$b$) $\Rightarrow$ $R$($b$,$a$) \\[0ex]5. $\forall$$a$, $b$, $c$:$T$. $R$($a$,$b$) $\Rightarrow$ $R$($b$,$c$) $\Rightarrow$ $R$($a$,$c$) \\[0ex]6. $a$ : $T$ \\[0ex]7. ${\it a'}$ : $T$ \\[0ex]8. $b$ : $T$ \\[0ex]9. ${\it b'}$ : $T$ \\[0ex]10. $R$($a$,$b$) \\[0ex]11. $R$(${\it a'}$,${\it b'}$) \\[0ex]12. $R$($a$,${\it a'}$) \\[0ex]$\vdash$ $R$($b$,${\it b'}$)